E:Type{i}, pred?:(E(?E)), X1,X2:Type{i}, info:(E((:Id  X1) + (:(:IdLnk  E)  X2))).
EOrderAxioms{i:l}(E; pred?; info)  prop{i':l} 

latex

Definitions	EOrderAxioms(E;pred?;info), x:A. B(x), P  Q, destination(l), SWellFounded(R(x;y)), x,y. t(x;y), pred!(e;e'), A, first(e), pred(e), P  Q, loc(e), source(l), b, rcv?(e), link(e), prop{i:l}, sender(e), P  Q, e < e', x:A. B(x), Id, IdLnk, Unit, t  T
Lemmas	unit wf, IdLnk wf, Id wf, cless wf, sender wf, link wf, rcv? wf, assert wf, lsrc wf, loc wf, pred wf, first wf, not wf, pred! wf, strongwellfounded wf, ldst wf